Inference at * 1 1 2 
Iof proof for Lemma decidable implies better:



1. P : 
2. Q : x:P.
3. P
4. P  Dec(Q)
  (P  Q)  ((P  Q)) 

latex

 by Assert (P  Q)   

latex

 1: .....assertion..... NILNIL

 1:   (P  Q)  
 2: 

 2: 5. (P  Q)  
 2:   (P  Q)  ((P  Q))
 .

Definitions

P  Q, , t  T